YES 22.828 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((maximum :: [Ratio Int ->  Ratio Int) :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((maximum :: [Ratio Int ->  Ratio Int) :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
max x y
 | x <= y
 = y
 | otherwise
 = x

is transformed to
max x y = max2 x y

max1 x y True = y
max1 x y False = max0 x y otherwise

max0 x y True = x

max2 x y = max1 x y (x <= y)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (maximum :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx4500), Succ(vx3101000)) → new_primPlusNat(vx4500, vx3101000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vx300000), vx310100) → new_primMulNat(vx300000, vx310100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx30800), Succ(vx44900)) → new_not(vx30800, vx44900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vx30, :(vx310, vx311)) → new_foldl(new_max1(vx30, vx310), vx311)

The TRS R consists of the following rules:

new_max151(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1120(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1106(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max116(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_max188(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max172(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max148(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1118(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max116(vx30100, vx31000000, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → new_max144(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max173(vx20, Neg(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Zero) → new_max1135(vx20, vx2100, vx2200, vx23, new_not7(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max193(vx31, Pos(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Zero) → new_max10(vx31, vx3200, vx3300, vx34, new_not7(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max193(vx31, Pos(Zero), Neg(Zero), vx34, Succ(vx2170)) → new_max114(vx31, vx34)
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max179(vx30100, vx310000, vx310100, new_not6(new_primPlusNat0(new_primMulNat0(vx310000, vx30100), Succ(vx30100))))
new_max193(vx31, Neg(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Succ(vx2170)) → new_max1144(vx31, vx3200, vx3300, vx34, new_not8(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200)), vx2170))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max155(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max173(vx20, Neg(Zero), Pos(Succ(vx2200)), vx23, Succ(vx1300)) → new_max1136(vx20, vx2200, vx23)
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1108(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max120(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max152(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max173(vx20, Neg(Zero), Neg(Succ(vx2200)), vx23, Zero) → new_max1141(vx20, Zero, Succ(vx2200), vx23)
new_max173(vx20, Neg(Succ(vx2100)), Neg(Zero), vx23, Zero) → new_max1141(vx20, Succ(vx2100), Zero, vx23)
new_max160(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max15(vx36, Neg(Succ(vx3700)), Neg(Zero), vx39, Zero) → :%(Neg(Zero), Neg(Succ(vx39)))
new_max158(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max154(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max133(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Neg(Zero), Pos(Succ(vx3800)), vx39, Zero) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_max15(vx36, Pos(Succ(vx3700)), Pos(Zero), vx39, Zero) → :%(Pos(Zero), Neg(Succ(vx39)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max171(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1122(vx30000, vx30100, True) → :%(Neg(Succ(Zero)), Neg(Zero))
new_max1142(vx20, vx2100, vx2200, vx23, True) → :%(Neg(Succ(vx2200)), Neg(Succ(vx23)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max181(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max145(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1127(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → new_max1102(vx30100, vx310100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1147(vx31, vx3200, vx34) → :%(Neg(Zero), Pos(Succ(vx34)))
new_max1141(vx20, vx210, vx220, vx23) → :%(Neg(vx220), Neg(Succ(vx23)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max1105(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max163(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1133(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max03(:%(Neg(Zero), Neg(Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1121(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max1112(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max159(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max124(vx15, Pos(Succ(vx1600)), Pos(Zero), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_max165(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max1119(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max126(vx15, vx1600, vx1700, vx18, False) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_max175(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max1122(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max188(vx30100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max140(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max132(vx30000, vx30100, True) → :%(Neg(Succ(Zero)), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max197(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_not4new_not5
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max165(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max173(vx20, Neg(Succ(vx2100)), Pos(Zero), vx23, Succ(vx1300)) → new_max115(vx20, vx2100, vx23)
new_max156(vx30000, vx30100, True) → :%(Pos(Succ(Zero)), Pos(Zero))
new_max118(vx30100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_not9new_not5
new_max189(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max02(vx15, vx160, vx170, vx18) → :%(Pos(Succ(vx15)), Neg(vx160))
new_max124(vx15, Neg(vx160), Pos(vx170), vx18, Succ(vx460)) → new_max02(vx15, vx160, vx170, vx18)
new_max113(vx31, vx3200, vx34) → :%(Pos(Zero), Pos(Succ(vx34)))
new_max1114(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max188(vx30100, True) → :%(Pos(Succ(Zero)), Neg(Zero))
new_max150(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max150(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max172(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max1100(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Neg(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Zero) → new_max17(vx36, vx3700, vx3800, vx39, new_not1(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max127(vx15, vx1600, vx1700, vx18, False) → new_max02(vx15, Succ(vx1600), Succ(vx1700), vx18)
new_max1127(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max11(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max185(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max193(vx31, Neg(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Zero) → new_max1144(vx31, vx3200, vx3300, vx34, new_not7(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_max1131(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max153(vx30100, vx31000000, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max127(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max196(vx30000, vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max138(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_not10(Succ(vx30800), Zero) → new_not3
new_max10(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx31)), Pos(Succ(vx3200)))
new_max15(vx36, Pos(Succ(vx3700)), Neg(Zero), vx39, Zero) → :%(Neg(Zero), Neg(Succ(vx39)))
new_max190(vx30100, vx31000000, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max124(vx15, Neg(Zero), Neg(Succ(vx1700)), vx18, Zero) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_max1115(vx30100, True) → :%(Neg(Succ(Zero)), Pos(Zero))
new_max165(vx30100, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max03(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max1113(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max124(vx15, Pos(Zero), Pos(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_max166(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max1130(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1130(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max172(vx30100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max1116(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max193(vx31, Neg(Zero), Pos(Zero), vx34, Succ(vx2170)) → new_max1145(vx31, vx34)
new_max1132(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max193(vx31, Pos(Succ(vx3200)), Neg(Zero), vx34, Zero) → new_max1147(vx31, vx3200, vx34)
new_max180(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max138(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_not0(vx3080, Succ(vx4490)) → new_not10(vx3080, vx4490)
new_max140(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_not1(Succ(vx4470)) → new_not8(Zero, vx4470)
new_not3False
new_max1101(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max131(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max150(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max193(vx31, Pos(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Zero) → new_max1148(vx31, vx3200, vx3300, vx34, new_not6(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_max1138(vx20, vx2100, vx2200, vx23, True) → :%(Neg(Succ(vx2200)), Neg(Succ(vx23)))
new_max18(vx36, vx3700, vx3800, vx39, False) → new_max0(vx36, Succ(vx3700), Succ(vx3800), vx39)
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max143(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1100(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_not6(Zero) → new_not4
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max1121(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max179(vx5, vx6, vx7, True) → :%(Pos(Succ(vx6)), Neg(Succ(vx7)))
new_max1112(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → new_max121(vx30100, :%(Neg(Succ(Zero)), Neg(Succ(vx310100))))
new_max124(vx15, Pos(Zero), Pos(Succ(vx1700)), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Pos(Zero))
new_max1116(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1121(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max1104(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max173(vx20, Neg(Succ(vx2100)), Pos(Zero), vx23, Zero) → new_max115(vx20, vx2100, vx23)
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max159(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max163(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(Zero)), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → new_max1108(vx30100, vx310100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max161(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_primMulNat0(Succ(vx300000), vx310100) → new_primPlusNat1(new_primMulNat0(vx300000, vx310100), vx310100)
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max118(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Neg(Zero), Pos(Zero), vx39, Zero) → :%(Pos(Zero), Neg(Succ(vx39)))
new_max1124(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max179(vx5, vx6, vx7, False) → :%(Pos(Zero), Pos(Succ(vx5)))
new_max158(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max164(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max146(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max11(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max168(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), vx301), :%(vx3100, Pos(Succ(vx310100)))) → new_max193(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_max195(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max156(vx30000, vx30100, False) → new_max03(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_max174(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max173(vx20, Pos(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Zero) → new_max1138(vx20, vx2100, vx2200, vx23, new_not7(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_max1134(vx20, vx2100, vx23) → :%(Neg(Zero), Neg(Succ(vx23)))
new_max193(vx31, Pos(Zero), Neg(Succ(vx3300)), vx34, Zero) → new_max1146(vx31, vx3300, vx34)
new_not0(vx3080, Zero) → new_not3
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max183(vx30100, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max128(vx15, vx1600, vx1700, vx18, False) → new_max01(vx15, Succ(vx1600), Succ(vx1700), vx18)
new_max178(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max182(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max14(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max151(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1105(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max193(vx31, Pos(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Succ(vx2170)) → new_max10(vx31, vx3200, vx3300, vx34, new_not8(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200)), vx2170))
new_max193(vx31, Neg(vx320), Neg(vx330), vx34, Succ(vx2170)) → new_max111(vx31, vx320, vx330, vx34)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max0(vx36, vx370, vx380, vx39) → :%(Neg(Succ(vx36)), Neg(vx370))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max15(vx36, Neg(Zero), Neg(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1129(vx30100, vx310100, True) → :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))
new_max124(vx15, Neg(Zero), Neg(Zero), vx18, Zero) → :%(Neg(Zero), Pos(Succ(vx18)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_max134(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max192(vx30100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max124(vx15, Pos(Zero), Pos(Zero), vx18, Zero) → :%(Pos(Zero), Pos(Succ(vx18)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max186(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max12(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max192(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → new_max121(vx30100, :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → new_max121(vx30100, :%(Neg(Zero), Pos(Zero)))
new_max139(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max1101(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max194(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max147(vx30100, vx31000000, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max193(vx31, Pos(Succ(vx3200)), Neg(Zero), vx34, Succ(vx2170)) → new_max1147(vx31, vx3200, vx34)
new_max1114(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max1128(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max173(vx20, Neg(Zero), Pos(Succ(vx2200)), vx23, Zero) → new_max1136(vx20, vx2200, vx23)
new_max131(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max160(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max163(vx30100, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1123(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1125(vx30100, vx310100, True) → :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))
new_max133(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max155(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1102(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max154(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max124(vx15, Pos(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Zero) → new_max125(vx15, vx1600, vx1700, vx18, new_not1(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max182(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Zero), Neg(Zero)))
new_max1104(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max1117(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max187(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max194(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), vx301), :%(vx3100, Neg(Succ(vx310100)))) → new_max173(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max152(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1109(vx30100, vx31000000, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max168(vx30100, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max193(vx31, Neg(Zero), Pos(Succ(vx3300)), vx34, Zero) → new_max141(vx31, vx3300, vx34)
new_max142(vx30100, vx31000000, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max155(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_max121(vx30100, :%(Neg(Succ(Zero)), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → new_max121(vx30100, :%(Pos(Zero), Neg(Succ(vx310100))))
new_max15(vx36, Neg(Zero), Neg(Zero), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → new_max121(vx30100, :%(Neg(Zero), Pos(Succ(vx310100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max183(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_primPlusNat1(Zero, vx310100) → Succ(vx310100)
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1144(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx31)), Neg(Succ(vx3200)))
new_max157(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max15(vx36, Pos(Succ(vx3700)), Pos(Zero), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → new_max1125(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max184(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_not10(Succ(vx30800), Succ(vx44900)) → new_not10(vx30800, vx44900)
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max164(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max124(vx15, Pos(Zero), Pos(Zero), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max132(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max124(vx15, Pos(Succ(vx1600)), Neg(Zero), vx18, Zero) → :%(Neg(Zero), Pos(Succ(vx18)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max1126(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1138(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx20)), Pos(Succ(vx2100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max193(vx31, Pos(Zero), Pos(Zero), vx34, Zero) → new_max1143(vx31, Zero, Zero, vx34)
new_max112(vx30100, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max171(vx30100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max124(vx15, Neg(Succ(vx1600)), Pos(Zero), vx18, Zero) → :%(Pos(Zero), Pos(Succ(vx18)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max174(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max129(vx30100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max157(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max193(vx31, Neg(Succ(vx3200)), Pos(Zero), vx34, Zero) → new_max113(vx31, vx3200, vx34)
new_max1137(vx20, vx23) → :%(Pos(Zero), Neg(Succ(vx23)))
new_max189(vx30100, vx31000000, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max199(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max186(vx30100, vx31000000, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1145(vx31, vx34) → :%(Pos(Zero), Pos(Succ(vx34)))
new_max193(vx31, Pos(Zero), Neg(Succ(vx3300)), vx34, Succ(vx2170)) → new_max1146(vx31, vx3300, vx34)
new_max111(vx31, vx320, vx330, vx34) → :%(Neg(vx330), Pos(Succ(vx34)))
new_max19(vx36, vx3700, vx3800, vx39, False) → new_max00(vx36, Succ(vx3700), Succ(vx3800), vx39)
new_max171(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max130(vx10) → :%(Neg(Zero), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max191(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → new_max1129(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max187(vx30100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max110(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max124(vx15, Pos(Zero), Neg(Succ(vx1700)), vx18, Zero) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_max133(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max144(vx30100, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max142(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max177(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max13(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_max1114(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max147(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max152(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max123(vx30100, vx31000000, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max125(vx15, vx1600, vx1700, vx18, False) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_max1100(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1129(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1115(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max03(vx537) → vx537
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max03(:%(Pos(Zero), Neg(Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_max132(vx30000, vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max15(vx36, Pos(Zero), Neg(Zero), vx39, Zero) → :%(Neg(Zero), Neg(Succ(vx39)))
new_primPlusNat0(Succ(vx4500), Zero) → Succ(vx4500)
new_primPlusNat0(Zero, Succ(vx3101000)) → Succ(vx3101000)
new_max1112(vx30100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max193(vx31, Neg(Zero), Neg(Zero), vx34, Zero) → new_max111(vx31, Zero, Zero, vx34)
new_max01(vx15, vx160, vx170, vx18) → :%(Pos(Succ(vx15)), Pos(vx160))
new_max15(vx36, Pos(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Zero) → new_max19(vx36, vx3700, vx3800, vx39, new_not2(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max123(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_not2(Zero) → new_not4
new_max187(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max168(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max13(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max15(vx36, Neg(Succ(vx3700)), Pos(Zero), vx39, Zero) → :%(Pos(Zero), Neg(Succ(vx39)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max177(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max124(vx15, Pos(Zero), Neg(Zero), vx18, Zero) → :%(Neg(Zero), Pos(Succ(vx18)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max148(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max12(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_not8(Succ(vx4130), vx2170) → new_not10(vx4130, vx2170)
new_max1111(vx30100, vx31000000, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1143(vx31, vx320, vx330, vx34) → :%(Pos(vx330), Pos(Succ(vx34)))
new_max190(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max192(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_primMulNat0(Zero, vx310100) → Zero
new_max1119(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx310000)), Neg(Zero))
new_max199(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_max145(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_not6(Succ(vx3990)) → new_not9
new_max143(vx30100, vx31000000, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max160(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max121(vx12, vx13) → vx13
new_max1(:%(Neg(Succ(vx30000)), vx301), :%(vx3100, Neg(Succ(vx310100)))) → new_max15(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max151(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max1127(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max145(vx30000, vx30100, True) → :%(Neg(Succ(Zero)), Pos(Zero))
new_max11(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max193(vx31, Pos(vx320), Pos(vx330), vx34, Succ(vx2170)) → new_max1143(vx31, vx320, vx330, vx34)
new_max1125(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_not1(Zero) → new_not4
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max124(vx15, Neg(Zero), Neg(Succ(vx1700)), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Neg(Zero))
new_max1108(vx30100, vx310100, True) → :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max110(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max15(vx36, Pos(Zero), Pos(Succ(vx3800)), vx39, Zero) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_max173(vx20, Neg(Zero), Neg(Zero), vx23, Zero) → new_max1141(vx20, Zero, Zero, vx23)
new_max173(vx20, Neg(Zero), Pos(Zero), vx23, Succ(vx1300)) → new_max1137(vx20, vx23)
new_max169(vx30100, vx31000000, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1136(vx20, vx2200, vx23) → :%(Pos(Succ(vx2200)), Neg(Succ(vx23)))
new_max124(vx15, Neg(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Zero) → new_max126(vx15, vx1600, vx1700, vx18, new_not1(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max122(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max1111(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → new_max121(vx30100, :%(Neg(Succ(Zero)), Pos(Succ(vx310100))))
new_max1133(vx30100, vx31000000, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max144(vx30100, vx310100, True) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max198(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max162(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Zero), Pos(Zero)))
new_max149(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_max1111(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max135(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max170(vx30100, False) → new_max03(:%(Pos(Zero), Pos(Succ(vx30100))))
new_max162(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max14(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_max1110(vx30100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max148(vx30100, vx31000000, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1103(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1123(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1119(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1126(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1140(vx20, vx23) → :%(Neg(Zero), Neg(Succ(vx23)))
new_max191(vx30100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max193(vx31, Neg(Zero), Neg(Succ(vx3300)), vx34, Zero) → new_max111(vx31, Zero, Succ(vx3300), vx34)
new_max193(vx31, Neg(Succ(vx3200)), Neg(Zero), vx34, Zero) → new_max111(vx31, Succ(vx3200), Zero, vx34)
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Zero), Pos(Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Succ(vx30000)), Pos(Zero)))
new_max115(vx20, vx2100, vx23) → :%(Pos(Zero), Neg(Succ(vx23)))
new_max173(vx20, Pos(Zero), Neg(Succ(vx2200)), vx23, Zero) → new_max1139(vx20, vx2200, vx23)
new_max184(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → new_max121(vx30100, :%(Pos(Zero), Pos(Succ(vx310100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max169(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max12(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max193(vx31, Neg(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Zero) → new_max1149(vx31, vx3200, vx3300, vx34, new_not6(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_max173(vx20, Neg(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Zero) → new_max1142(vx20, vx2100, vx2200, vx23, new_not6(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max167(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max198(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max185(vx30100, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max15(vx36, Neg(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Zero) → new_max18(vx36, vx3700, vx3800, vx39, new_not2(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max185(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max00(vx36, vx370, vx380, vx39) → :%(Neg(Succ(vx36)), Pos(vx370))
new_max195(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max173(vx20, Pos(vx210), Pos(vx220), vx23, Succ(vx1300)) → new_max119(vx20, vx210, vx220, vx23)
new_max196(vx30000, vx30100, False) → new_max03(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_max110(vx30100, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max189(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Pos(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Succ(vx3080)) → new_max16(vx36, vx3700, vx3800, vx39, new_not0(vx3080, new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max176(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max153(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max138(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max177(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max16(vx36, vx3700, vx3800, vx39, True) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_primPlusNat0(Zero, Zero) → Zero
new_max173(vx20, Pos(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Succ(vx1300)) → new_max1138(vx20, vx2100, vx2200, vx23, new_not8(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100)), vx1300))
new_max193(vx31, Pos(Zero), Neg(Zero), vx34, Zero) → new_max114(vx31, vx34)
new_max1135(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx20)), Neg(Succ(vx2100)))
new_max124(vx15, Neg(Succ(vx1600)), Neg(Zero), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_max15(vx36, Neg(Zero), Neg(Zero), vx39, Zero) → :%(Neg(Zero), Neg(Succ(vx39)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max13(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max114(vx31, vx34) → :%(Neg(Zero), Pos(Succ(vx34)))
new_max173(vx20, Neg(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Succ(vx1300)) → new_max1135(vx20, vx2100, vx2200, vx23, new_not8(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100)), vx1300))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1126(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max158(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max129(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max139(vx30100, True) → :%(Neg(Succ(Zero)), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1130(vx30100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_primPlusNat1(Succ(vx450), vx310100) → Succ(Succ(new_primPlusNat0(vx450, vx310100)))
new_max134(vx30000, vx30100, True) → :%(Pos(Succ(Zero)), Neg(Zero))
new_max124(vx15, Neg(Zero), Neg(Zero), vx18, Succ(vx460)) → :%(Pos(Succ(vx15)), Neg(Zero))
new_max15(vx36, Neg(Zero), Neg(Succ(vx3800)), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Neg(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Succ(vx30000)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Zero), Neg(Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Pos(Succ(vx30000)), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Zero), Pos(Succ(vx30100))))
new_max119(vx20, vx210, vx220, vx23) → :%(Pos(vx220), Neg(Succ(vx23)))
new_max197(vx30000, vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max157(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1139(vx20, vx2200, vx23) → :%(Neg(Succ(vx2200)), Neg(Succ(vx23)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max183(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → new_max121(vx30100, :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max1128(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max1107(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1101(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_max1115(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max124(vx15, Neg(Zero), Pos(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_max124(vx15, Neg(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Succ(vx460)) → new_max126(vx15, vx1600, vx1700, vx18, new_not0(vx460, new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max173(vx20, Pos(Zero), Pos(Succ(vx2200)), vx23, Zero) → new_max119(vx20, Zero, Succ(vx2200), vx23)
new_max173(vx20, Pos(Succ(vx2100)), Pos(Zero), vx23, Zero) → new_max119(vx20, Succ(vx2100), Zero, vx23)
new_max1105(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max176(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max161(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1132(vx30100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1102(vx30100, vx310100, True) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max15(vx36, Neg(Succ(vx3700)), Neg(Zero), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_max173(vx20, Pos(Succ(vx2100)), Neg(Zero), vx23, Zero) → new_max1134(vx20, vx2100, vx23)
new_max17(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max1110(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max193(vx31, Pos(Zero), Pos(Succ(vx3300)), vx34, Zero) → new_max1143(vx31, Zero, Succ(vx3300), vx34)
new_max193(vx31, Pos(Succ(vx3200)), Pos(Zero), vx34, Zero) → new_max1143(vx31, Succ(vx3200), Zero, vx34)
new_max173(vx20, Pos(Zero), Neg(Zero), vx23, Zero) → new_max1140(vx20, vx23)
new_max1117(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max122(vx30100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max15(vx36, Pos(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Zero) → new_max16(vx36, vx3700, vx3800, vx39, new_not1(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max143(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max125(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_max193(vx31, Neg(Succ(vx3200)), Pos(Zero), vx34, Succ(vx2170)) → new_max113(vx31, vx3200, vx34)
new_max191(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_max1116(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max134(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max124(vx15, Pos(Succ(vx1600)), Pos(Zero), vx18, Zero) → :%(Pos(Zero), Pos(Succ(vx18)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_max121(vx30100, :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max184(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1107(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max175(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Pos(Zero), Pos(Succ(vx3800)), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max137(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max170(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → new_max121(vx30100, :%(Neg(Zero), Neg(Succ(vx310100))))
new_max120(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max128(vx15, vx1600, vx1700, vx18, True) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_max15(vx36, Neg(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Succ(vx3080)) → new_max17(vx36, vx3700, vx3800, vx39, new_not0(vx3080, new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_max117(vx30100, vx31000000, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max182(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max129(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1131(vx30100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max196(vx30000, vx30100, True) → :%(Pos(Succ(Zero)), Pos(Zero))
new_max137(vx30100, False) → new_max03(:%(Neg(Zero), Pos(Succ(vx30100))))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max1118(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max117(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max03(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_max154(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max124(vx15, Neg(Zero), Pos(Zero), vx18, Zero) → :%(Pos(Zero), Pos(Succ(vx18)))
new_max198(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1107(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max146(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max124(vx15, Pos(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Succ(vx460)) → new_max125(vx15, vx1600, vx1700, vx18, new_not0(vx460, new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max166(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max131(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max178(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_not10(Zero, Zero) → new_not4
new_max186(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max1133(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max164(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max120(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_max124(vx15, Neg(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Zero) → new_max127(vx15, vx1600, vx1700, vx18, new_not2(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max173(vx20, Pos(Succ(vx2100)), Neg(Zero), vx23, Succ(vx1300)) → new_max1134(vx20, vx2100, vx23)
new_max1144(vx31, vx3200, vx3300, vx34, True) → :%(Pos(Succ(vx3300)), Pos(Succ(vx34)))
new_max1104(vx30100, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max118(vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max1146(vx31, vx3300, vx34) → :%(Neg(Succ(vx3300)), Pos(Succ(vx34)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max1109(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1113(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_not2(Succ(vx4520)) → new_not3
new_max1131(vx30100, True) → :%(Pos(Succ(Zero)), Neg(Zero))
new_max1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max195(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_max149(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1128(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max1149(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx3300)), Pos(Succ(vx34)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_max139(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max123(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max15(vx36, Pos(Zero), Pos(Zero), vx39, Succ(vx3080)) → :%(Neg(Succ(vx36)), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max126(vx15, vx1600, vx1700, vx18, True) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_max1110(vx30100, True) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_max18(vx36, vx3700, vx3800, vx39, True) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_max1148(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx31)), Pos(Succ(vx3200)))
new_max173(vx20, Pos(Zero), Neg(Zero), vx23, Succ(vx1300)) → new_max1140(vx20, vx23)
new_max1124(vx30100, vx310100, True) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max1124(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max178(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max136(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx20)), Pos(Succ(vx2100)))
new_max1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(Zero)), Neg(Zero))
new_max1113(vx30100, vx31000000, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max173(vx20, Neg(Zero), Pos(Zero), vx23, Zero) → new_max1137(vx20, vx23)
new_max117(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max147(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max124(vx15, Pos(vx160), Neg(vx170), vx18, Succ(vx460)) → new_max01(vx15, vx160, vx170, vx18)
new_max199(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1103(vx30100, vx31000000, vx310100, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_not7(Succ(vx4110)) → new_not0(vx4110, Zero)
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max1123(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_not10(Zero, Succ(vx44900)) → new_not9
new_max15(vx36, Neg(vx370), Pos(vx380), vx39, Succ(vx3080)) → new_max0(vx36, vx370, vx380, vx39)
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_max181(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max176(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max16(vx36, vx3700, vx3800, vx39, False) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max153(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max10(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx3300)), Pos(Succ(vx34)))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_max112(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max1148(vx31, vx3200, vx3300, vx34, True) → :%(Pos(Succ(vx3300)), Pos(Succ(vx34)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max197(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max15(vx36, Pos(Zero), Pos(Zero), vx39, Zero) → :%(Pos(Zero), Neg(Succ(vx39)))
new_max173(vx20, Pos(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Zero) → new_max136(vx20, vx2100, vx2200, vx23, new_not6(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_max166(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max19(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_max167(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max1120(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max169(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1109(vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Succ(vx30000)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_max130(:%(Neg(Zero), Neg(Succ(vx30100))))
new_max159(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_max181(vx30100, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_primPlusNat0(Succ(vx4500), Succ(vx3101000)) → Succ(Succ(new_primPlusNat0(vx4500, vx3101000)))
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max193(vx31, Neg(Zero), Pos(Zero), vx34, Zero) → new_max1145(vx31, vx34)
new_max173(vx20, Neg(vx210), Neg(vx220), vx23, Succ(vx1300)) → new_max1141(vx20, vx210, vx220, vx23)
new_max193(vx31, Neg(Zero), Pos(Succ(vx3300)), vx34, Succ(vx2170)) → new_max141(vx31, vx3300, vx34)
new_max1120(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max124(vx15, Pos(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Zero) → new_max128(vx15, vx1600, vx1700, vx18, new_not2(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_max112(vx30100, vx310100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_max141(vx31, vx3300, vx34) → :%(Pos(Succ(vx3300)), Pos(Succ(vx34)))
new_max1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max180(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max116(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_max1118(vx30000, vx30100, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max137(vx30100, True) → :%(Pos(Succ(Zero)), Pos(Zero))
new_max1106(vx30100, vx31000000, vx310100, False) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_not5True
new_max173(vx20, Pos(Zero), Neg(Succ(vx2200)), vx23, Succ(vx1300)) → new_max1139(vx20, vx2200, vx23)
new_max167(vx30100, vx31000000, vx310100, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_max122(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max170(vx30100, True) → :%(Pos(Succ(Zero)), Pos(Zero))
new_not7(Zero) → new_not4
new_max1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_max156(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_not8(Zero, vx2170) → new_not9
new_max1135(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx2200)), Neg(Succ(vx23)))
new_max1149(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx31)), Neg(Succ(vx3200)))
new_max140(vx30000, vx30100, True) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_max161(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max190(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max15(vx36, Pos(vx370), Neg(vx380), vx39, Succ(vx3080)) → new_max00(vx36, vx370, vx380, vx39)
new_max136(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx2200)), Neg(Succ(vx23)))
new_max17(vx36, vx3700, vx3800, vx39, False) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_max1142(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx20)), Neg(Succ(vx2100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx310000)), Pos(Zero))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Succ(vx310100)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx310000)), Neg(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_max14(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max194(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_max1122(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_max135(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_max146(vx30100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max1106(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max124(vx15, Neg(Succ(vx1600)), Neg(Zero), vx18, Zero) → :%(Neg(Zero), Pos(Succ(vx18)))
new_max1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_max1132(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_max175(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_max1(:%(Pos(Succ(vx30000)), vx301), :%(vx3100, Pos(Succ(vx310100)))) → new_max124(vx30000, vx301, vx3100, vx310100, new_primPlusNat1(new_primMulNat0(vx30000, vx310100), vx310100))
new_max174(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_max162(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_max1117(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max15(vx36, Pos(Zero), Neg(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_max142(vx30100, vx31000000, True) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_max1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_max1103(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max180(vx30100, vx31000000, vx310100, False) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_max1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_max135(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_max173(vx20, Pos(Zero), Pos(Zero), vx23, Zero) → new_max119(vx20, Zero, Zero, vx23)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx310000)), Pos(Zero))
new_max149(vx30000, vx30100, False) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx310100)))

The set Q consists of the following terms:

new_not7(Zero)
new_max1110(x0, True)
new_max194(x0, x1, x2, False)
new_max119(x0, x1, x2, x3)
new_max15(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_max15(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max150(x0, x1, False)
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max192(x0, True)
new_max146(x0, False)
new_max1143(x0, x1, x2, x3)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_max1103(x0, x1, x2, False)
new_max17(x0, x1, x2, x3, True)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max186(x0, x1, True)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_max174(x0, x1, x2, False)
new_max193(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_max162(x0, x1, x2, False)
new_max124(x0, Neg(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_max173(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_max173(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_max149(x0, x1, True)
new_max124(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_max132(x0, x1, True)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max128(x0, x1, x2, x3, True)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max134(x0, x1, True)
new_max125(x0, x1, x2, x3, False)
new_max178(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1112(x0, False)
new_max1123(x0, x1, x2, True)
new_max144(x0, x1, False)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_max1142(x0, x1, x2, x3, False)
new_max1111(x0, x1, False)
new_max117(x0, x1, True)
new_max124(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_max00(x0, x1, x2, x3)
new_max167(x0, x1, x2, False)
new_max198(x0, x1, x2, False)
new_max1147(x0, x1, x2)
new_max163(x0, x1, False)
new_max1(:%(Pos(Succ(x0)), x1), :%(x2, Pos(Succ(x3))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max1101(x0, x1, False)
new_max1111(x0, x1, True)
new_max11(x0, x1, True)
new_max118(x0, False)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1145(x0, x1)
new_max1107(x0, x1, True)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_max171(x0, True)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1138(x0, x1, x2, x3, True)
new_max1126(x0, x1, x2, True)
new_max126(x0, x1, x2, x3, False)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_max124(x0, Neg(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_max19(x0, x1, x2, x3, False)
new_max1136(x0, x1, x2)
new_max173(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_max150(x0, x1, True)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_max1149(x0, x1, x2, x3, True)
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_max1142(x0, x1, x2, x3, True)
new_max176(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max193(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_max177(x0, x1, False)
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_max1130(x0, True)
new_max127(x0, x1, x2, x3, True)
new_max15(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_max15(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_max193(x0, Neg(x1), Neg(x2), x3, Succ(x4))
new_max1105(x0, x1, x2, False)
new_max156(x0, x1, False)
new_max173(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_max180(x0, x1, x2, True)
new_max15(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_max15(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_max15(x0, Pos(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_max193(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_max193(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_max14(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_max196(x0, x1, False)
new_max1113(x0, x1, False)
new_max155(x0, x1, False)
new_max181(x0, x1, False)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max124(x0, Pos(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_max110(x0, x1, False)
new_max154(x0, x1, x2, True)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_max167(x0, x1, x2, True)
new_max1119(x0, x1, True)
new_not10(Zero, Succ(x0))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_max1146(x0, x1, x2)
new_max141(x0, x1, x2)
new_not10(Succ(x0), Succ(x1))
new_max193(x0, Neg(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_not7(Succ(x0))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_max193(x0, Pos(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_max145(x0, x1, True)
new_max1104(x0, x1, True)
new_max1115(x0, False)
new_max1108(x0, x1, True)
new_max139(x0, False)
new_max149(x0, x1, False)
new_max15(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max124(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_max163(x0, x1, True)
new_max183(x0, x1, False)
new_primPlusNat0(Succ(x0), Zero)
new_max113(x0, x1, x2)
new_max1125(x0, x1, True)
new_max173(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_max1114(x0, True)
new_max173(x0, Pos(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_max173(x0, Neg(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_max122(x0, False)
new_max14(x0, x1, x2, False)
new_max185(x0, x1, True)
new_max124(x0, Pos(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_max1121(x0, x1, True)
new_max155(x0, x1, True)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max195(x0, x1, True)
new_max1131(x0, True)
new_max1126(x0, x1, x2, False)
new_max173(x0, Pos(Zero), Neg(Zero), x1, Succ(x2))
new_max173(x0, Neg(Zero), Pos(Zero), x1, Succ(x2))
new_max1122(x0, x1, False)
new_max139(x0, True)
new_max1123(x0, x1, x2, False)
new_max1127(x0, x1, True)
new_max166(x0, x1, x2, True)
new_max193(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_max1112(x0, True)
new_max125(x0, x1, x2, x3, True)
new_max1139(x0, x1, x2)
new_max124(x0, Pos(Zero), Pos(Zero), x1, Succ(x2))
new_max193(x0, Neg(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_max193(x0, Pos(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_primPlusNat0(Zero, Succ(x0))
new_not8(Succ(x0), x1)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max121(x0, x1)
new_not6(Zero)
new_max1121(x0, x1, False)
new_max122(x0, True)
new_max156(x0, x1, True)
new_max111(x0, x1, x2, x3)
new_max173(x0, Pos(x1), Pos(x2), x3, Succ(x4))
new_max12(x0, x1, x2, False)
new_max117(x0, x1, False)
new_max168(x0, x1, False)
new_max136(x0, x1, x2, x3, True)
new_max187(x0, False)
new_max173(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_max173(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_max193(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_max193(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_max161(x0, x1, x2, False)
new_max15(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_max185(x0, x1, False)
new_max124(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max190(x0, x1, False)
new_max153(x0, x1, False)
new_max13(x0, x1, x2, True)
new_max1119(x0, x1, False)
new_max15(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max147(x0, x1, True)
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max132(x0, x1, False)
new_max124(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_max15(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_max1127(x0, x1, False)
new_max165(x0, x1, False)
new_max16(x0, x1, x2, x3, False)
new_max1115(x0, True)
new_max140(x0, x1, True)
new_max15(x0, Pos(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_max112(x0, x1, False)
new_max116(x0, x1, False)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_max187(x0, True)
new_max124(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_max124(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max126(x0, x1, x2, x3, True)
new_not8(Zero, x0)
new_max1144(x0, x1, x2, x3, True)
new_max195(x0, x1, False)
new_primPlusNat0(Zero, Zero)
new_max1113(x0, x1, True)
new_max173(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_max173(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_max198(x0, x1, x2, True)
new_max1110(x0, False)
new_max188(x0, False)
new_primMulNat0(Succ(x0), x1)
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1105(x0, x1, x2, True)
new_max1122(x0, x1, True)
new_max1120(x0, x1, x2, False)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max142(x0, x1, False)
new_max190(x0, x1, True)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max151(x0, True)
new_max164(x0, x1, x2, True)
new_max1132(x0, True)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(x1)), Neg(Succ(x2))))
new_max1135(x0, x1, x2, x3, True)
new_max124(x0, Pos(x1), Neg(x2), x3, Succ(x4))
new_max124(x0, Neg(x1), Pos(x2), x3, Succ(x4))
new_max145(x0, x1, False)
new_max184(x0, x1, x2, True)
new_max1138(x0, x1, x2, x3, False)
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_max178(x0, x1, x2, False)
new_max1114(x0, False)
new_max118(x0, True)
new_max1137(x0, x1)
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_max193(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1148(x0, x1, x2, x3, True)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_max1118(x0, x1, False)
new_max193(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max193(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max138(x0, x1, True)
new_max173(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_not1(Succ(x0))
new_not3
new_max127(x0, x1, x2, x3, False)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max175(x0, x1, True)
new_max15(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_max161(x0, x1, x2, True)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_max172(x0, True)
new_max1130(x0, False)
new_not2(Succ(x0))
new_max193(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max02(x0, x1, x2, x3)
new_max189(x0, x1, False)
new_max176(x0, x1, x2, False)
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_max123(x0, x1, True)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_max12(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_primMulNat0(Zero, x0)
new_max18(x0, x1, x2, x3, False)
new_max115(x0, x1, x2)
new_max130(x0)
new_max193(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_max1118(x0, x1, True)
new_max1140(x0, x1)
new_max193(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_max193(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_max137(x0, False)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_max182(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_max169(x0, x1, True)
new_max120(x0, x1, x2, False)
new_primPlusNat1(Succ(x0), x1)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_max1134(x0, x1, x2)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_max183(x0, x1, True)
new_max124(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_max1125(x0, x1, False)
new_max18(x0, x1, x2, x3, True)
new_max124(x0, Neg(Zero), Neg(Zero), x1, Succ(x2))
new_max169(x0, x1, False)
new_max10(x0, x1, x2, x3, False)
new_max158(x0, x1, False)
new_not2(Zero)
new_max172(x0, False)
new_max124(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_max124(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_max01(x0, x1, x2, x3)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_not5
new_max191(x0, False)
new_max180(x0, x1, x2, False)
new_max1108(x0, x1, False)
new_max159(x0, x1, x2, True)
new_max184(x0, x1, x2, False)
new_not6(Succ(x0))
new_max10(x0, x1, x2, x3, True)
new_max181(x0, x1, True)
new_max124(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_max191(x0, True)
new_not10(Succ(x0), Zero)
new_max193(x0, Pos(x1), Pos(x2), x3, Succ(x4))
new_max1131(x0, False)
new_primPlusNat0(Succ(x0), Succ(x1))
new_max199(x0, x1, x2, True)
new_max1(:%(Neg(Succ(x0)), x1), :%(x2, Neg(Succ(x3))))
new_max1148(x0, x1, x2, x3, False)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_max173(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_max173(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_max124(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max124(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max147(x0, x1, False)
new_max196(x0, x1, True)
new_max15(x0, Pos(x1), Neg(x2), x3, Succ(x4))
new_max15(x0, Neg(x1), Pos(x2), x3, Succ(x4))
new_max189(x0, x1, True)
new_max1133(x0, x1, True)
new_max1133(x0, x1, False)
new_max1106(x0, x1, x2, False)
new_max143(x0, x1, True)
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_max175(x0, x1, False)
new_max162(x0, x1, x2, True)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max148(x0, x1, False)
new_max151(x0, False)
new_max131(x0, x1, True)
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_max143(x0, x1, False)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max168(x0, x1, True)
new_max199(x0, x1, x2, False)
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max112(x0, x1, True)
new_max133(x0, x1, True)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_max1103(x0, x1, x2, True)
new_max138(x0, x1, False)
new_max1117(x0, x1, x2, True)
new_max110(x0, x1, True)
new_max170(x0, True)
new_max179(x0, x1, x2, True)
new_max1128(x0, x1, False)
new_max0(x0, x1, x2, x3)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_max1120(x0, x1, x2, True)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_max157(x0, x1, x2, False)
new_max135(x0, x1, x2, True)
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max1(:%(Neg(Succ(x0)), x1), :%(x2, Pos(Succ(x3))))
new_max1(:%(Pos(Succ(x0)), x1), :%(x2, Neg(Succ(x3))))
new_max174(x0, x1, x2, True)
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max15(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_max13(x0, x1, x2, False)
new_max1128(x0, x1, True)
new_max1102(x0, x1, True)
new_max128(x0, x1, x2, x3, False)
new_primPlusNat1(Zero, x0)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_max15(x0, Neg(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_max173(x0, Neg(x1), Neg(x2), x3, Succ(x4))
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max120(x0, x1, x2, True)
new_max1132(x0, False)
new_max116(x0, x1, True)
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_max164(x0, x1, x2, False)
new_max144(x0, x1, True)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_max1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_max152(x0, True)
new_max1101(x0, x1, True)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max136(x0, x1, x2, x3, False)
new_max188(x0, True)
new_max1104(x0, x1, False)
new_not0(x0, Succ(x1))
new_max186(x0, x1, False)
new_max133(x0, x1, False)
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_max1100(x0, x1, x2, True)
new_max1144(x0, x1, x2, x3, False)
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1124(x0, x1, True)
new_max173(x0, Pos(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_max173(x0, Neg(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_max11(x0, x1, False)
new_max152(x0, False)
new_max135(x0, x1, x2, False)
new_max173(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max193(x0, Neg(Zero), Pos(Zero), x1, Succ(x2))
new_max193(x0, Pos(Zero), Neg(Zero), x1, Succ(x2))
new_max1102(x0, x1, False)
new_max177(x0, x1, True)
new_max15(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_max197(x0, x1, False)
new_max160(x0, x1, False)
new_not1(Zero)
new_max193(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_max193(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_max15(x0, Neg(Zero), Neg(Zero), x1, Succ(x2))
new_max158(x0, x1, True)
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max15(x0, Neg(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max140(x0, x1, False)
new_not4
new_max193(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_max194(x0, x1, x2, True)
new_max192(x0, False)
new_max157(x0, x1, x2, True)
new_max171(x0, False)
new_not0(x0, Zero)
new_max134(x0, x1, False)
new_max1124(x0, x1, False)
new_max154(x0, x1, x2, False)
new_max1106(x0, x1, x2, True)
new_max1109(x0, x1, True)
new_not10(Zero, Zero)
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max173(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_max1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max173(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_max148(x0, x1, True)
new_max124(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_max1141(x0, x1, x2, x3)
new_max124(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_max124(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_max16(x0, x1, x2, x3, True)
new_max193(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max146(x0, True)
new_max173(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_max160(x0, x1, True)
new_max1116(x0, x1, x2, True)
new_max129(x0, True)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_max153(x0, x1, True)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_max159(x0, x1, x2, False)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_max165(x0, x1, True)
new_max1129(x0, x1, True)
new_max1117(x0, x1, x2, False)
new_max129(x0, False)
new_max182(x0, x1, x2, False)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_max179(x0, x1, x2, False)
new_max1109(x0, x1, False)
new_max19(x0, x1, x2, x3, True)
new_max15(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max15(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max1149(x0, x1, x2, x3, False)
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_max166(x0, x1, x2, False)
new_max170(x0, False)
new_max1116(x0, x1, x2, False)
new_max123(x0, x1, False)
new_max15(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_max173(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_max1107(x0, x1, False)
new_max1129(x0, x1, False)
new_max1135(x0, x1, x2, x3, False)
new_max17(x0, x1, x2, x3, False)
new_max15(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_max197(x0, x1, True)
new_not9
new_max114(x0, x1)
new_max1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_max1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_max131(x0, x1, False)
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_max1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_max03(x0)
new_max137(x0, True)
new_max142(x0, x1, True)
new_max15(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_max1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_max1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_max124(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_max124(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_max1100(x0, x1, x2, False)
new_max173(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_max15(x0, Pos(Zero), Pos(Zero), x1, Succ(x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: